\begin{tabbing}
R{-}frame{-}compat($A$;$B$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=i\=f \=Reffect?($A$)$\rightarrow$\+\+\+
\\[0ex]i\=f Rframe?($B$)$\rightarrow$ Rframe{-}x($B$) $=$ Reffect{-}x($A$) $\Rightarrow$ (Reffect{-}knd($A$) $\in$ Rframe{-}L($B$))\+
\\[0ex]; Raframe?($B$)$\rightarrow$ Raframe{-}k($B$) $=$ Reffect{-}knd($A$) $\Rightarrow$ (Reffect{-}x($A$) $\in$ Raframe{-}L($B$))
\\[0ex]; \=Rrframe?($B$)$\rightarrow$\+
\\[0ex]Rrframe{-}x($B$) $\in$ dom(Reffect{-}ds($A$)) $\Rightarrow$ (Reffect{-}knd($A$) $\in$ Rrframe{-}L($B$))
\-\-\\[0ex]else True fi
\-\\[0ex]; \=Rsends?($A$)$\rightarrow$\+
\\[0ex]i\=f \=Rsframe?($B$)$\rightarrow$\+\+
\\[0ex]Rsframe{-}lnk($B$) $=$ Rsends{-}l($A$)
\\[0ex]$\Rightarrow$ (Rsframe{-}tag($B$) $\in$ map($\lambda$$p$.1of($p$);Rsends{-}g($A$)))
\\[0ex]$\Rightarrow$ (Rsends{-}knd($A$) $\in$ Rsframe{-}L($B$))
\-\\[0ex]; Rbframe?($B$)$\rightarrow$ Rbframe{-}k($B$) $=$ Rsends{-}knd($A$) $\Rightarrow$ (Rsends{-}l($A$) $\in$ Rbframe{-}L($B$))
\\[0ex]; Rrframe?($B$)$\rightarrow$ Rrframe{-}x($B$) $\in$ dom(Rsends{-}ds($A$)) $\Rightarrow$ (Rsends{-}knd($A$) $\in$ Rrframe{-}L($B$))
\-\\[0ex]else True fi
\-\\[0ex]; \=Rpre?($A$)$\rightarrow$\+
\\[0ex]if Rrframe?($B$)$\rightarrow$ Rrframe{-}x($B$) $\in$ dom(Rpre{-}ds($A$)) $\Rightarrow$ (locl(Rpre{-}a($A$)) $\in$ Rrframe{-}L($B$))
\\[0ex]else True fi
\-\-\\[0ex]else True fi
\-
\end{tabbing}